Nuprl Lemma : concat-cons
0,22
postcript
pdf
l
:Top List,
ll
:(Top List) List. concat(
l
.
ll
) ~ (
l
@ concat(
ll
))
latex
Definitions
concat(
ll
)
,
x
:
A
.
B
(
x
)
,
t
T
,
Top
Lemmas
top
wf
origin
l:Top List, ll:(Top List) List. concat(l.ll) ~ (l @ concat(ll)) l:Top List, ll:(Top List) List. concat(l.ll) ~ (l @ concat(ll)) x:A. B(x)
T